chain-config(es;Sys;chain)
== (e:E(Sys). no_repeats(Id;chain(e)) & (0 < ||chain(e)||) & (loc(e)  chain(e)))
== & (e, e':E(Sys). chain(e)  chain(e')  chain(e')  chain(e))
== & (e, e':E(Sys). (e <loc e')  chain(e')  chain(e)) 

latex

---

clarification:

chain-config(es;Sys;chain)
== (e:es-E-interface(es;Sys).
== (no_repeats(Id;chain(e)) & (0 < ||chain(e)||) & (es-loc(es; e)  chain(e)  Id))
== & (e:es-E-interface(es;Sys), e':es-E-interface(es;Sys).
== & (sublist(Id; (chain(e)); (chain(e')))  sublist(Id; (chain(e')); (chain(e))))
== & (e:es-E-interface(es;Sys), e':es-E-interface(es;Sys).
== & (es-locl(es; e; e')  sublist(Id; (chain(e')); (chain(e)))) 

latex

Up	abstract chain replication
Wellformedness Lemmas	chain-config wf
Definitions	no_repeats(T;l), a < b, #$n, ||as||, (x  l), loc(e), P & Q, P  Q, x:A. B(x), E(X), P  Q, (e <loc e'), L1  L2, Id, f(a)
FDL editor aliases	chain-config